Nuprl Lemma : retraction_wf
11,40
postcript
pdf
T
:Type,
f
:(
T
T
). retraction(
T
;
f
)
latex
Definitions
Type
,
t
T
,
s
=
t
,
x
:
A
B
(
x
)
,
,
{
x
:
A
|
B
(
x
)}
,
,
|
g
|
,
S
T
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
a
<
b
,
,
left
+
right
,
P
Q
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
retraction(
T
;
f
)
Lemmas
nat
wf
origin
T:Type, f:(T
T). retraction(T;f) 
T:Type, f:(TT). retraction(T;f) TB(x)
Tx:A. B(x)
Q
B(x)
x:A. B(x)